COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "let.pub" source
C00005 ENDMK
C⊗;
.require "let.pub" source
.font D "Grkl30"
.font E "sup"
.font F "math30"
.turn on "⊗" for "#"
∂AIL Dr. J Strother Moore↓SRI International↓333 Ravenswood Ave.
↓Menlo Park CA 94025∞

Dear J:

	Enclosed is another proof of the correctness of %2tak%1
from A. Nozaki, whom I don't remember having met.  I have read the
proof, and I believe it.  I think it can be converted into
a lexicographic proof or, as I like to think of it, an induction
up to %Dw%E2%1.  It covers the real case also, and its inductions
are unequivocally on non-negative integers only.  The amount of real
arithmetic that has to be axiomatized to justify it seems trivial.
Off hand it looks like we need to know that the reals are totally
ordered, that %Fi%2x%Fj%1 is monotonic and that it satisfies
%Fi%2x⊗-⊗%11%Fj%2⊗=⊗%Fi%2x%Fj%1⊗-⊗1.
Richard plans to do the Nozaki proof in FOL.

	I read yours and balked at the possibility that subtractions
that are set to zero rather than being allowed to go negative might
affect its correctness.  Unfortunately, I don't have time to reread
it and see if I still balk.

	Enclosed is an %2Elephant%1.  I suppose your system could
do Elephant proofs also, since Elephant programs are also just sentences
of first order logic, but maybe the heuristics are too different.
Your reaction would be interesting.

.reg